#pragma once

#include "mockturtle/mockturtle.hpp"
#include <alloca.h>
#include <cstdint>
#include <exception>
#include <iostream>
#include <string>
#include <unordered_map>
#include <vector>

template<class TT>
bool bottom_mux_decomposition( const TT& tt, uint32_t sel, uint32_t var_index1, uint32_t var_index2, TT* func = nullptr )
{
  const auto co0_var1 = cofactor0( tt, var_index1 );
  const auto co1_var1 = cofactor1( tt, var_index1 );
  const auto dif_var1 = kitty::binary_xor( co0_var1, co1_var1 );

  const auto co0_var2 = cofactor0( tt, var_index2 );
  const auto co1_var2 = cofactor1( tt, var_index2 );
  const auto dif_var2 = kitty::binary_xor( co0_var2, co1_var2 );

  const auto dif1_co0_var2 = cofactor0( dif_var1, var_index2 );
  const auto dif1_co1_var2 = cofactor1( dif_var1, var_index2 );
  const auto dif1_dif2 = kitty::binary_xor( dif1_co0_var2, dif1_co1_var2 );

  const auto co1_dif1_sel = cofactor1( dif_var1, sel );
  const auto co0_dif2_sel = cofactor0( dif_var2, sel );

  const auto co0_var1_var2 = cofactor0( cofactor0( tt, var_index1 ), var_index2 );
  const auto co1_var1_var2 = cofactor1( cofactor1( tt, var_index1 ), var_index2 );

  const auto dif0_sel = kitty::binary_xor( cofactor0( co0_var1_var2, sel ), cofactor1( co0_var1_var2, sel ) );
  const auto dif1_sel = kitty::binary_xor( cofactor0( co1_var1_var2, sel ), cofactor1( co1_var1_var2, sel ) );

  const auto co0_dif1_sel = cofactor0( dif_var1, sel );

  if ( equal( dif_var1, dif_var2 ) )
  {
    return false;
  }

  if ( is_const0( dif1_dif2 ) & is_const0( co1_dif1_sel ) & is_const0( co0_dif2_sel ) & is_const0( dif0_sel ) & is_const0( dif1_sel ) )
  {
    if ( func )
    {
      const auto co0_dif1_sel = cofactor0( dif_var1, sel );
      kitty::dynamic_truth_table tt_1( co0_dif1_sel.num_vars() );
      *func = kitty::binary_xor( mux_var( sel, co0_dif1_sel, tt_1 ), co0_var1_var2 );
    }
    return true;
  }
  return false;
}

template<class TT>
bool top_mux_decomposition( const TT& tt, uint32_t var_index1, TT* func_co0 = nullptr, TT* func_co1 = nullptr )
{
  static_assert( kitty::is_complete_truth_table<TT>::value, "Can only be applied on complete truth tables." );
  bool has_decomp = true;
  const auto co0_var1 = cofactor0( tt, var_index1 );
  const auto co1_var1 = cofactor1( tt, var_index1 );
  std::vector<uint8_t> support_co0;
  std::vector<uint8_t> support_co1;
  for ( auto s_sd = 0u; s_sd < co0_var1.num_vars(); ++s_sd )
  {
    if ( kitty::has_var( co0_var1, s_sd ) )
    {
      support_co0.push_back( s_sd );
    }
  }
  for ( auto s_sd = 0u; s_sd < co1_var1.num_vars(); ++s_sd )
  {
    if ( kitty::has_var( co1_var1, s_sd ) )
    {
      support_co1.push_back( s_sd );
    }
  }

  for ( auto i = 0u; i < support_co0.size(); ++i )
  {
    if ( has_decomp == false )
    {
      break;
    }
    for ( auto j = 0u; j < support_co0.size(); ++j )
    {
      if ( support_co0[i] == support_co1[j] )
      {
        has_decomp = false;
        break;
      }
    }
  }
  if ( has_decomp )
  {
    if ( func_co0 )
    {
      *func_co0 = co0_var1;
    }
    if ( func_co1 )
    {
      *func_co1 = co1_var1;
    }
    return true;
  }
  return false;
}